The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(1(x1))) → 0(2(1(1(x1))))
0(1(1(x1))) → 0(0(2(1(1(x1)))))
0(1(1(x1))) → 0(2(1(2(1(x1)))))
0(1(1(x1))) → 2(1(0(2(1(x1)))))
3(0(1(x1))) → 1(3(0(0(2(4(x1))))))
3(5(1(x1))) → 1(3(4(5(x1))))
3(5(1(x1))) → 2(4(5(3(1(x1)))))
5(1(3(x1))) → 5(3(1(2(x1))))
0(1(0(1(x1)))) → 1(1(0(0(2(4(x1))))))
0(1(2(3(x1)))) → 3(1(5(0(2(x1)))))
0(1(2(3(x1)))) → 0(3(1(2(1(1(x1))))))
0(1(4(1(x1)))) → 0(2(1(2(4(1(x1))))))
0(1(4(1(x1)))) → 4(0(0(2(1(1(x1))))))
0(1(5(1(x1)))) → 0(0(2(1(1(5(x1))))))
0(4(5(1(x1)))) → 0(1(3(4(5(x1)))))
3(2(0(1(x1)))) → 1(3(0(2(4(5(x1))))))
3(5(1(1(x1)))) → 1(3(4(5(1(x1)))))
3(5(1(1(x1)))) → 1(5(3(1(2(x1)))))
3(5(1(3(x1)))) → 3(5(3(1(2(x1)))))
3(5(4(1(x1)))) → 4(1(3(4(5(x1)))))
5(1(2(3(x1)))) → 5(5(3(1(2(x1)))))
5(2(0(1(x1)))) → 5(3(1(0(2(4(x1))))))
5(4(3(3(x1)))) → 3(1(3(4(5(x1)))))
5(5(0(1(x1)))) → 1(0(2(4(5(5(x1))))))
0(1(2(0(1(x1))))) → 0(3(0(2(1(1(x1))))))
0(1(2(2(1(x1))))) → 0(2(1(2(1(3(x1))))))
0(3(0(5(1(x1))))) → 0(3(4(5(0(1(x1))))))
0(3(4(2(3(x1))))) → 0(5(3(4(3(2(x1))))))
0(3(5(4(1(x1))))) → 0(5(2(4(3(1(x1))))))
0(4(1(2(3(x1))))) → 0(3(2(4(5(1(x1))))))
0(4(1(2(3(x1))))) → 4(3(1(0(0(2(x1))))))
0(4(5(5(1(x1))))) → 2(4(5(5(0(1(x1))))))
0(5(1(0(1(x1))))) → 0(1(5(5(0(1(x1))))))
0(5(3(2(1(x1))))) → 0(0(2(5(3(1(x1))))))
3(0(1(2(3(x1))))) → 0(2(3(4(3(1(x1))))))
3(0(1(2(3(x1))))) → 1(1(3(3(0(2(x1))))))
3(0(1(2(3(x1))))) → 1(2(3(3(0(2(x1))))))
3(0(4(1(1(x1))))) → 0(0(1(3(4(1(x1))))))
3(2(4(1(3(x1))))) → 4(3(4(3(1(2(x1))))))
3(3(4(1(1(x1))))) → 1(3(4(5(3(1(x1))))))
3(3(5(1(1(x1))))) → 3(1(4(5(3(1(x1))))))
3(5(4(1(3(x1))))) → 1(4(5(3(1(3(x1))))))
3(5(4(4(1(x1))))) → 4(1(4(3(4(5(x1))))))
5(2(4(2(3(x1))))) → 3(2(4(5(3(2(x1))))))
5(4(2(0(1(x1))))) → 5(1(2(0(2(4(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(1(z0))) → c(0'(2(1(1(z0)))))
0'(1(1(z0))) → c1(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(1(z0))) → c2(0'(2(1(2(1(z0))))))
0'(1(1(z0))) → c3(0'(2(1(z0))))
0'(1(0(1(z0)))) → c4(0'(0(2(4(z0)))), 0'(2(4(z0))))
0'(1(2(3(z0)))) → c5(3'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
0'(1(2(3(z0)))) → c6(0'(3(1(2(1(1(z0)))))), 3'(1(2(1(1(z0))))))
0'(1(4(1(z0)))) → c7(0'(2(1(2(4(1(z0)))))))
0'(1(4(1(z0)))) → c8(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(5(1(z0)))) → c9(0'(0(2(1(1(5(z0)))))), 0'(2(1(1(5(z0))))), 5'(z0))
0'(4(5(1(z0)))) → c10(0'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
0'(1(2(0(1(z0))))) → c11(0'(3(0(2(1(1(z0)))))), 3'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
0'(3(0(5(1(z0))))) → c13(0'(3(4(5(0(1(z0)))))), 3'(4(5(0(1(z0))))), 5'(0(1(z0))), 0'(1(z0)))
0'(3(4(2(3(z0))))) → c14(0'(5(3(4(3(2(z0)))))), 5'(3(4(3(2(z0))))), 3'(4(3(2(z0)))), 3'(2(z0)))
0'(3(5(4(1(z0))))) → c15(0'(5(2(4(3(1(z0)))))), 5'(2(4(3(1(z0))))), 3'(1(z0)))
0'(4(1(2(3(z0))))) → c16(0'(3(2(4(5(1(z0)))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
0'(4(1(2(3(z0))))) → c17(3'(1(0(0(2(z0))))), 0'(0(2(z0))), 0'(2(z0)))
0'(4(5(5(1(z0))))) → c18(5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(1(0(1(z0))))) → c19(0'(1(5(5(0(1(z0)))))), 5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(3(2(1(z0))))) → c20(0'(0(2(5(3(1(z0)))))), 0'(2(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(0(1(z0))) → c21(3'(0(0(2(4(z0))))), 0'(0(2(4(z0)))), 0'(2(4(z0))))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(5(1(z0))) → c23(5'(3(1(z0))), 3'(1(z0)))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(1(1(z0)))) → c25(3'(4(5(1(z0)))), 5'(1(z0)))
3'(5(1(1(z0)))) → c26(5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(1(3(z0)))) → c27(3'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(0(1(2(3(z0))))) → c29(0'(2(3(4(3(1(z0)))))), 3'(4(3(1(z0)))), 3'(1(z0)))
3'(0(1(2(3(z0))))) → c30(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(0(1(2(3(z0))))) → c31(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(0(4(1(1(z0))))) → c32(0'(0(1(3(4(1(z0)))))), 0'(1(3(4(1(z0))))), 3'(4(1(z0))))
3'(2(4(1(3(z0))))) → c33(3'(4(3(1(2(z0))))), 3'(1(2(z0))))
3'(3(4(1(1(z0))))) → c34(3'(4(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(3(5(1(1(z0))))) → c35(3'(1(4(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(1(3(z0))) → c38(5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(1(2(3(z0)))) → c39(5'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(2(0(1(z0)))) → c40(5'(3(1(0(2(4(z0)))))), 3'(1(0(2(4(z0))))), 0'(2(4(z0))))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
5'(4(2(0(1(z0))))) → c44(5'(1(2(0(2(4(z0)))))), 0'(2(4(z0))))

S tuples:

0'(1(1(z0))) → c(0'(2(1(1(z0)))))
0'(1(1(z0))) → c1(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(1(z0))) → c2(0'(2(1(2(1(z0))))))
0'(1(1(z0))) → c3(0'(2(1(z0))))
0'(1(0(1(z0)))) → c4(0'(0(2(4(z0)))), 0'(2(4(z0))))
0'(1(2(3(z0)))) → c5(3'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
0'(1(2(3(z0)))) → c6(0'(3(1(2(1(1(z0)))))), 3'(1(2(1(1(z0))))))
0'(1(4(1(z0)))) → c7(0'(2(1(2(4(1(z0)))))))
0'(1(4(1(z0)))) → c8(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(5(1(z0)))) → c9(0'(0(2(1(1(5(z0)))))), 0'(2(1(1(5(z0))))), 5'(z0))
0'(4(5(1(z0)))) → c10(0'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
0'(1(2(0(1(z0))))) → c11(0'(3(0(2(1(1(z0)))))), 3'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
0'(3(0(5(1(z0))))) → c13(0'(3(4(5(0(1(z0)))))), 3'(4(5(0(1(z0))))), 5'(0(1(z0))), 0'(1(z0)))
0'(3(4(2(3(z0))))) → c14(0'(5(3(4(3(2(z0)))))), 5'(3(4(3(2(z0))))), 3'(4(3(2(z0)))), 3'(2(z0)))
0'(3(5(4(1(z0))))) → c15(0'(5(2(4(3(1(z0)))))), 5'(2(4(3(1(z0))))), 3'(1(z0)))
0'(4(1(2(3(z0))))) → c16(0'(3(2(4(5(1(z0)))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
0'(4(1(2(3(z0))))) → c17(3'(1(0(0(2(z0))))), 0'(0(2(z0))), 0'(2(z0)))
0'(4(5(5(1(z0))))) → c18(5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(1(0(1(z0))))) → c19(0'(1(5(5(0(1(z0)))))), 5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(3(2(1(z0))))) → c20(0'(0(2(5(3(1(z0)))))), 0'(2(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(0(1(z0))) → c21(3'(0(0(2(4(z0))))), 0'(0(2(4(z0)))), 0'(2(4(z0))))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(5(1(z0))) → c23(5'(3(1(z0))), 3'(1(z0)))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(1(1(z0)))) → c25(3'(4(5(1(z0)))), 5'(1(z0)))
3'(5(1(1(z0)))) → c26(5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(1(3(z0)))) → c27(3'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(0(1(2(3(z0))))) → c29(0'(2(3(4(3(1(z0)))))), 3'(4(3(1(z0)))), 3'(1(z0)))
3'(0(1(2(3(z0))))) → c30(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(0(1(2(3(z0))))) → c31(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(0(4(1(1(z0))))) → c32(0'(0(1(3(4(1(z0)))))), 0'(1(3(4(1(z0))))), 3'(4(1(z0))))
3'(2(4(1(3(z0))))) → c33(3'(4(3(1(2(z0))))), 3'(1(2(z0))))
3'(3(4(1(1(z0))))) → c34(3'(4(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(3(5(1(1(z0))))) → c35(3'(1(4(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(1(3(z0))) → c38(5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(1(2(3(z0)))) → c39(5'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(2(0(1(z0)))) → c40(5'(3(1(0(2(4(z0)))))), 3'(1(0(2(4(z0))))), 0'(2(4(z0))))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
5'(4(2(0(1(z0))))) → c44(5'(1(2(0(2(4(z0)))))), 0'(2(4(z0))))

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

0'(1(0(1(z0)))) → c4(0'(0(2(4(z0)))), 0'(2(4(z0))))
0'(1(2(3(z0)))) → c5(3'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
0'(1(2(3(z0)))) → c6(0'(3(1(2(1(1(z0)))))), 3'(1(2(1(1(z0))))))
0'(1(5(1(z0)))) → c9(0'(0(2(1(1(5(z0)))))), 0'(2(1(1(5(z0))))), 5'(z0))
0'(4(5(1(z0)))) → c10(0'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
0'(1(2(0(1(z0))))) → c11(0'(3(0(2(1(1(z0)))))), 3'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(3(0(5(1(z0))))) → c13(0'(3(4(5(0(1(z0)))))), 3'(4(5(0(1(z0))))), 5'(0(1(z0))), 0'(1(z0)))
0'(3(4(2(3(z0))))) → c14(0'(5(3(4(3(2(z0)))))), 5'(3(4(3(2(z0))))), 3'(4(3(2(z0)))), 3'(2(z0)))
0'(3(5(4(1(z0))))) → c15(0'(5(2(4(3(1(z0)))))), 5'(2(4(3(1(z0))))), 3'(1(z0)))
0'(4(1(2(3(z0))))) → c16(0'(3(2(4(5(1(z0)))))), 3'(2(4(5(1(z0))))), 5'(1(z0)))
0'(4(1(2(3(z0))))) → c17(3'(1(0(0(2(z0))))), 0'(0(2(z0))), 0'(2(z0)))
0'(4(5(5(1(z0))))) → c18(5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(1(0(1(z0))))) → c19(0'(1(5(5(0(1(z0)))))), 5'(5(0(1(z0)))), 5'(0(1(z0))), 0'(1(z0)))
0'(5(3(2(1(z0))))) → c20(0'(0(2(5(3(1(z0)))))), 0'(2(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(1(3(z0)))) → c27(3'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(0(1(2(3(z0))))) → c29(0'(2(3(4(3(1(z0)))))), 3'(4(3(1(z0)))), 3'(1(z0)))
3'(0(1(2(3(z0))))) → c30(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(0(1(2(3(z0))))) → c31(3'(3(0(2(z0)))), 3'(0(2(z0))), 0'(2(z0)))
3'(3(5(1(1(z0))))) → c35(3'(1(4(5(3(1(z0)))))), 5'(3(1(z0))), 3'(1(z0)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(1(z0))) → c(0'(2(1(1(z0)))))
0'(1(1(z0))) → c1(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(1(z0))) → c2(0'(2(1(2(1(z0))))))
0'(1(1(z0))) → c3(0'(2(1(z0))))
0'(1(4(1(z0)))) → c7(0'(2(1(2(4(1(z0)))))))
0'(1(4(1(z0)))) → c8(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
3'(0(1(z0))) → c21(3'(0(0(2(4(z0))))), 0'(0(2(4(z0)))), 0'(2(4(z0))))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(5(1(z0))) → c23(5'(3(1(z0))), 3'(1(z0)))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(1(1(z0)))) → c25(3'(4(5(1(z0)))), 5'(1(z0)))
3'(5(1(1(z0)))) → c26(5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(0(4(1(1(z0))))) → c32(0'(0(1(3(4(1(z0)))))), 0'(1(3(4(1(z0))))), 3'(4(1(z0))))
3'(2(4(1(3(z0))))) → c33(3'(4(3(1(2(z0))))), 3'(1(2(z0))))
3'(3(4(1(1(z0))))) → c34(3'(4(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(1(3(z0))) → c38(5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(1(2(3(z0)))) → c39(5'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(2(0(1(z0)))) → c40(5'(3(1(0(2(4(z0)))))), 3'(1(0(2(4(z0))))), 0'(2(4(z0))))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
5'(4(2(0(1(z0))))) → c44(5'(1(2(0(2(4(z0)))))), 0'(2(4(z0))))

S tuples:

0'(1(1(z0))) → c(0'(2(1(1(z0)))))
0'(1(1(z0))) → c1(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(1(z0))) → c2(0'(2(1(2(1(z0))))))
0'(1(1(z0))) → c3(0'(2(1(z0))))
0'(1(4(1(z0)))) → c7(0'(2(1(2(4(1(z0)))))))
0'(1(4(1(z0)))) → c8(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
3'(0(1(z0))) → c21(3'(0(0(2(4(z0))))), 0'(0(2(4(z0)))), 0'(2(4(z0))))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(5(1(z0))) → c23(5'(3(1(z0))), 3'(1(z0)))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(1(1(z0)))) → c25(3'(4(5(1(z0)))), 5'(1(z0)))
3'(5(1(1(z0)))) → c26(5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(0(4(1(1(z0))))) → c32(0'(0(1(3(4(1(z0)))))), 0'(1(3(4(1(z0))))), 3'(4(1(z0))))
3'(2(4(1(3(z0))))) → c33(3'(4(3(1(2(z0))))), 3'(1(2(z0))))
3'(3(4(1(1(z0))))) → c34(3'(4(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(1(3(z0))) → c38(5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(1(2(3(z0)))) → c39(5'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(2(0(1(z0)))) → c40(5'(3(1(0(2(4(z0)))))), 3'(1(0(2(4(z0))))), 0'(2(4(z0))))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
5'(4(2(0(1(z0))))) → c44(5'(1(2(0(2(4(z0)))))), 0'(2(4(z0))))

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c, c1, c2, c3, c7, c8, c12, c21, c22, c23, c24, c25, c26, c28, c32, c33, c34, c36, c37, c38, c39, c40, c41, c42, c43, c44

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 17 of 26 dangling nodes:

3'(2(4(1(3(z0))))) → c33(3'(4(3(1(2(z0))))), 3'(1(2(z0))))
0'(1(1(z0))) → c(0'(2(1(1(z0)))))
3'(3(4(1(1(z0))))) → c34(3'(4(5(3(1(z0))))), 5'(3(1(z0))), 3'(1(z0)))
0'(1(1(z0))) → c1(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
0'(1(1(z0))) → c2(0'(2(1(2(1(z0))))))
3'(0(4(1(1(z0))))) → c32(0'(0(1(3(4(1(z0)))))), 0'(1(3(4(1(z0))))), 3'(4(1(z0))))
0'(1(1(z0))) → c3(0'(2(1(z0))))
5'(1(3(z0))) → c38(5'(3(1(2(z0)))), 3'(1(2(z0))))
0'(1(4(1(z0)))) → c7(0'(2(1(2(4(1(z0)))))))
0'(1(4(1(z0)))) → c8(0'(0(2(1(1(z0))))), 0'(2(1(1(z0)))))
5'(1(2(3(z0)))) → c39(5'(5(3(1(2(z0))))), 5'(3(1(2(z0)))), 3'(1(2(z0))))
5'(2(0(1(z0)))) → c40(5'(3(1(0(2(4(z0)))))), 3'(1(0(2(4(z0))))), 0'(2(4(z0))))
5'(4(2(0(1(z0))))) → c44(5'(1(2(0(2(4(z0)))))), 0'(2(4(z0))))
3'(0(1(z0))) → c21(3'(0(0(2(4(z0))))), 0'(0(2(4(z0)))), 0'(2(4(z0))))
3'(5(1(z0))) → c23(5'(3(1(z0))), 3'(1(z0)))
3'(5(1(1(z0)))) → c26(5'(3(1(2(z0)))), 3'(1(2(z0))))
3'(5(1(1(z0)))) → c25(3'(4(5(1(z0)))), 5'(1(z0)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))

S tuples:

0'(1(2(2(1(z0))))) → c12(0'(2(1(2(1(3(z0)))))), 3'(z0))
3'(5(1(z0))) → c22(3'(4(5(z0))), 5'(z0))
3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(4(1(z0)))) → c28(3'(4(5(z0))), 5'(z0))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
3'(5(4(4(1(z0))))) → c37(3'(4(5(z0))), 5'(z0))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c12, c22, c24, c28, c36, c37, c41, c42, c43

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
0'(1(2(2(1(z0))))) → c(0'(2(1(2(1(3(z0)))))))
0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(3'(4(5(z0))))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(3'(4(5(z0))))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(3'(4(5(z0))))
3'(5(4(4(1(z0))))) → c(5'(z0))

S tuples:

3'(2(0(1(z0)))) → c24(3'(0(2(4(5(z0))))), 0'(2(4(5(z0)))), 5'(z0))
3'(5(4(1(3(z0))))) → c36(5'(3(1(3(z0)))), 3'(1(3(z0))), 3'(z0))
5'(4(3(3(z0)))) → c41(3'(1(3(4(5(z0))))), 3'(4(5(z0))), 5'(z0))
5'(5(0(1(z0)))) → c42(0'(2(4(5(5(z0))))), 5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(3'(2(4(5(3(2(z0)))))), 5'(3(2(z0))), 3'(2(z0)))
0'(1(2(2(1(z0))))) → c(0'(2(1(2(1(3(z0)))))))
0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(3'(4(5(z0))))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(3'(4(5(z0))))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(3'(4(5(z0))))
3'(5(4(4(1(z0))))) → c(5'(z0))

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5', 0'

Compound Symbols:

c24, c36, c41, c42, c43, c

(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 12 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(5'(3(2(z0))), 3'(2(z0)))
0'(1(2(2(1(z0))))) → c
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c

S tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(5'(3(2(z0))), 3'(2(z0)))
0'(1(2(2(1(z0))))) → c
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43, c

(11) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

0'(1(2(2(1(z0))))) → c(3'(z0))
0'(1(2(2(1(z0))))) → c

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(5'(3(2(z0))), 3'(2(z0)))
0'(1(2(2(1(z0))))) → c
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c

S tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(z0))))) → c43(5'(3(2(z0))), 3'(2(z0)))
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c

K tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
0'(1(2(2(1(z0))))) → c

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43, c

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 5'(2(4(2(3(z0))))) → c43(5'(3(2(z0))), 3'(2(z0))) by

5'(2(4(2(3(4(1(3(z0)))))))) → c43(5'(4(3(4(3(1(2(z0))))))), 3'(2(4(1(3(z0))))))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
0'(1(2(2(1(z0))))) → c
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c
5'(2(4(2(3(4(1(3(z0)))))))) → c43(5'(4(3(4(3(1(2(z0))))))), 3'(2(4(1(3(z0))))))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c
5'(2(4(2(3(4(1(3(z0)))))))) → c43(5'(4(3(4(3(1(2(z0))))))), 3'(2(4(1(3(z0))))))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

0'(1(2(2(1(z0))))) → c(3'(z0))
0'(1(2(2(1(z0))))) → c

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

0', 3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c, c43, c43

(15) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 6 of 14 dangling nodes:

0'(1(2(2(1(z0))))) → c
3'(5(1(z0))) → c
3'(5(4(1(z0)))) → c
3'(5(4(4(1(z0))))) → c
5'(2(4(2(3(4(1(3(z0)))))))) → c43(5'(4(3(4(3(1(2(z0))))))), 3'(2(4(1(3(z0))))))
0'(1(2(2(1(z0))))) → c(3'(z0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

3'(5(4(1(3(z0))))) → c36(3'(z0))

We considered the (Usable) Rules:

5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))

And the Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [4]   
POL(1(x₁)) = x₁   
POL(2(x₁)) = 0   
POL(3(x₁)) = [4] + [4]x₁   
POL(3'(x₁)) = [4]x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(5'(x₁)) = 0   
POL(c(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

3'(5(4(1(3(z0))))) → c36(3'(z0))

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(19) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

3'(2(0(1(z0)))) → c24(5'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

3'(5(4(1(3(z0))))) → c36(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

3'(2(0(1(z0)))) → c24(5'(z0))

We considered the (Usable) Rules:

5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))

And the Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [1] + [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = x₁   
POL(3'(x₁)) = [2]x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(5'(x₁)) = [2]x₁   
POL(c(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

3'(5(4(1(3(z0))))) → c36(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))

We considered the (Usable) Rules:

5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))

And the Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [4] + [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = x₁   
POL(3(x₁)) = x₁   
POL(3'(x₁)) = [1] + [2]x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(5'(x₁)) = [1] + [2]x₁   
POL(c(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c36(x₁)) = x₁   
POL(c41(x₁)) = x₁   
POL(c42(x₁, x₂)) = x₁ + x₂   
POL(c43(x₁)) = x₁   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

S tuples:

5'(4(3(3(z0)))) → c41(5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

3'(5(4(1(3(z0))))) → c36(3'(z0))
3'(5(1(z0))) → c(5'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace 3'(5(1(z0))) → c(5'(z0)) by

3'(5(1(4(3(3(y0)))))) → c(5'(4(3(3(y0)))))
3'(5(1(5(0(1(y0)))))) → c(5'(5(0(1(y0)))))
3'(5(1(2(4(2(3(y0))))))) → c(5'(2(4(2(3(y0))))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:

3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))
3'(5(1(4(3(3(y0)))))) → c(5'(4(3(3(y0)))))
3'(5(1(5(0(1(y0)))))) → c(5'(5(0(1(y0)))))
3'(5(1(2(4(2(3(y0))))))) → c(5'(2(4(2(3(y0))))))

S tuples:

5'(4(3(3(z0)))) → c41(5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))

K tuples:

3'(5(4(1(3(z0))))) → c36(3'(z0))
3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
3'(5(1(4(3(3(y0)))))) → c(5'(4(3(3(y0)))))
3'(5(1(5(0(1(y0)))))) → c(5'(5(0(1(y0)))))
3'(5(1(2(4(2(3(y0))))))) → c(5'(2(4(2(3(y0))))))

Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:

3', 5'

Compound Symbols:

c, c24, c36, c41, c42, c43

(27) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

3'(5(4(1(z0)))) → c(5'(z0))
3'(5(4(4(1(z0))))) → c(5'(z0))
3'(2(0(1(z0)))) → c24(5'(z0))
3'(5(4(1(3(z0))))) → c36(3'(z0))
5'(4(3(3(z0)))) → c41(5'(z0))
5'(5(0(1(z0)))) → c42(5'(5(z0)), 5'(z0))
5'(2(4(2(3(x0))))) → c43(3'(2(x0)))
3'(5(1(4(3(3(y0)))))) → c(5'(4(3(3(y0)))))
3'(5(1(5(0(1(y0)))))) → c(5'(5(0(1(y0)))))
3'(5(1(2(4(2(3(y0))))))) → c(5'(2(4(2(3(y0))))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(1(z0))) → 0(2(1(1(z0))))
0(1(1(z0))) → 0(0(2(1(1(z0)))))
0(1(1(z0))) → 0(2(1(2(1(z0)))))
0(1(1(z0))) → 2(1(0(2(1(z0)))))
0(1(0(1(z0)))) → 1(1(0(0(2(4(z0))))))
0(1(2(3(z0)))) → 3(1(5(0(2(z0)))))
0(1(2(3(z0)))) → 0(3(1(2(1(1(z0))))))
0(1(4(1(z0)))) → 0(2(1(2(4(1(z0))))))
0(1(4(1(z0)))) → 4(0(0(2(1(1(z0))))))
0(1(5(1(z0)))) → 0(0(2(1(1(5(z0))))))
0(4(5(1(z0)))) → 0(1(3(4(5(z0)))))
0(1(2(0(1(z0))))) → 0(3(0(2(1(1(z0))))))
0(1(2(2(1(z0))))) → 0(2(1(2(1(3(z0))))))
0(3(0(5(1(z0))))) → 0(3(4(5(0(1(z0))))))
0(3(4(2(3(z0))))) → 0(5(3(4(3(2(z0))))))
0(3(5(4(1(z0))))) → 0(5(2(4(3(1(z0))))))
0(4(1(2(3(z0))))) → 0(3(2(4(5(1(z0))))))
0(4(1(2(3(z0))))) → 4(3(1(0(0(2(z0))))))
0(4(5(5(1(z0))))) → 2(4(5(5(0(1(z0))))))
0(5(1(0(1(z0))))) → 0(1(5(5(0(1(z0))))))
0(5(3(2(1(z0))))) → 0(0(2(5(3(1(z0))))))
3(0(1(z0))) → 1(3(0(0(2(4(z0))))))
3(5(1(z0))) → 1(3(4(5(z0))))
3(5(1(z0))) → 2(4(5(3(1(z0)))))
3(2(0(1(z0)))) → 1(3(0(2(4(5(z0))))))
3(5(1(1(z0)))) → 1(3(4(5(1(z0)))))
3(5(1(1(z0)))) → 1(5(3(1(2(z0)))))
3(5(1(3(z0)))) → 3(5(3(1(2(z0)))))
3(5(4(1(z0)))) → 4(1(3(4(5(z0)))))
3(0(1(2(3(z0))))) → 0(2(3(4(3(1(z0))))))
3(0(1(2(3(z0))))) → 1(1(3(3(0(2(z0))))))
3(0(1(2(3(z0))))) → 1(2(3(3(0(2(z0))))))
3(0(4(1(1(z0))))) → 0(0(1(3(4(1(z0))))))
3(2(4(1(3(z0))))) → 4(3(4(3(1(2(z0))))))
3(3(4(1(1(z0))))) → 1(3(4(5(3(1(z0))))))
3(3(5(1(1(z0))))) → 3(1(4(5(3(1(z0))))))
3(5(4(1(3(z0))))) → 1(4(5(3(1(3(z0))))))
3(5(4(4(1(z0))))) → 4(1(4(3(4(5(z0))))))
5(1(3(z0))) → 5(3(1(2(z0))))
5(1(2(3(z0)))) → 5(5(3(1(2(z0)))))
5(2(0(1(z0)))) → 5(3(1(0(2(4(z0))))))
5(4(3(3(z0)))) → 3(1(3(4(5(z0)))))
5(5(0(1(z0)))) → 1(0(2(4(5(5(z0))))))
5(2(4(2(3(z0))))) → 3(2(4(5(3(2(z0))))))
5(4(2(0(1(z0))))) → 5(1(2(0(2(4(z0))))))

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

0, 3, 5

Defined Pair Symbols:none

Compound Symbols:none

(29) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(30) BOUNDS(O(1), O(1))